the proof LISPAX:

1. (DECL CAR (UNARYNAME: CAR) (TYPE: |GROUND→GROUND|) (SYNTYPE: CONSTANT)
     (BINDINGPOWER: 950))

2. (DECL CDR (UNARYNAME: CDR) (TYPE: |GROUND→GROUND|) (SYNTYPE: CONSTANT)
     (BINDINGPOWER: 950))

3. (DECL ATOM (UNARYNAME: ATOM) (TYPE: |GROUND→TRUTHVAL|) (SYNTYPE: CONSTANT)
     (BINDINGPOWER: 750))

4. (DECL NULL (UNARYNAME: NULL) (TYPE: |GROUND→TRUTHVAL|) (SYNTYPE: CONSTANT)
     (BINDINGPOWER: 750))

5. (DECL LISTP (UNARYNAME: LISTP) (TYPE: |GROUND→TRUTHVAL|) (SYNTYPE: CONSTANT)
     (BINDINGPOWER: 750))

6. (DECL ALISTP (UNARYNAME: ALISTP) (TYPE: |GROUND→TRUTHVAL|)
     (SYNTYPE: CONSTANT) (BINDINGPOWER: 750))

7. (DECL SEXP (UNARYNAME: SEXP) (TYPE: |GROUND→TRUTHVAL|) (SYNTYPE: CONSTANT)
     (BINDINGPOWER: 750))

8. (DECL (U V W) (TYPE: |GROUND|) (SORT: |LISTP|))

9. (DECL (X Y Z) (TYPE: |GROUND|) (SORT: |SEXP|))

10. (DECL (XA YA ZA) (TYPE: |GROUND|) (SORT: |ATOM|))

11. (DECL (A B C) (TYPE: |GROUND|))

12. (DECL (PHI) (TYPE: |GROUND→TRUTHVAL|))

13. (DECL CONS (TYPE: |(GROUND⊗GROUND)→GROUND|) (SYNTYPE: CONSTANT)
      (INFIXNAME: .) (PREFIXNAME: CONS) (BINDINGPOWER: 850))

;labels: SIMPINFO 
14. (AXIOM |∀XA.SEXP XA|)

;labels: SIMPINFO 
15. (AXIOM |∀U.SEXP U|)

;labels: SIMPINFO 
16. (AXIOM |∀X U.LISTP X.U|)

;labels: SIMPINFO 
17. (AXIOM |∀U.¬NULL U⊃LISTP CDR U|)

;labels: SIMPINFO 
18. (AXIOM |∀U.¬NULL U⊃SEXP CAR U|)

;labels: SIMPINFO 
19. (AXIOM |∀X.¬ATOM X⊃SEXP CAR X|)

;labels: SIMPINFO 
20. (AXIOM |∀X.¬ATOM X⊃SEXP CDR X|)

;labels: SIMPINFO 
21. (AXIOM |∀X Y.SEXP X.Y|)

;labels: SIMPINFO 
22. (AXIOM |∀X Y.¬ATOM X.Y|)

;labels: SIMPINFO 
23. (AXIOM |∀X U.¬NULL X.U|)

;labels: SIMPINFO 
24. (AXIOM |∀U.NULL U⊃U=NIL|)

;labels: SIMPINFO 
25. (AXIOM |∀X Y.CAR (X.Y)=X|)

;labels: SIMPINFO 
26. (AXIOM |∀X Y.CDR (X.Y)=Y|)

;labels: SIMPINFO 
27. (AXIOM |∀U.¬NULL U⊃CAR U.CDR U=U|)

;labels: SIMPINFO 
28. (AXIOM |∀X.¬ATOM X⊃CAR X.CDR X=X|)

;labels: LISTINDUCTION 
29. (AXIOM |∀PHI.PHI(NIL)∧(∀X U.PHI(U)⊃PHI(X.U))⊃(∀U.PHI(U))|)

30. (DECL PARS (TYPE: |GROUND*|))

31. (DECL (DF DF1 DF2) (TYPE: |(GROUND⊗(GROUND*))→(GROUND*)|))

32. (DECL NILCASE (TYPE: |(GROUND*)→(GROUND*)|))

;labels: LISTINDUCTIONDEF 
33. (AXIOM
      |∀DF NILCASE DEF.(∃FUN.(∀PARS X U.FUN(NIL,PARS)=NILCASE(PARS)∧
                                        FUN(X.U,PARS)=
                                        DEF(X,U,FUN(U,DF(X,PARS)),PARS)))|)

;labels: SEXPINDUCTION 
34. (AXIOM |∀PHI.(∀X.ATOM X⊃PHI(X))∧(∀X Y.PHI(X)∧PHI(Y)⊃PHI(X.Y))⊃(∀X.PHI(X))|)

;labels: SEXPINDUCTIONDEF 
35. (AXIOM
      |∀ATOMCASE DEFSEXP DF1 DF2.(∃FUN.(∀PARS X Y.(ATOM X⊃
                                                   FUN(X,PARS)=
                                                   ATOMCASE(X,PARS))∧
                                                  FUN(X.Y,PARS)=
                                                  DEFSEXP(X,Y,
                                                          FUN(X,DF1(X,PARS)),
                                                          FUN(Y,DF2(X,PARS)),
                                                          PARS)))|)

36. (DECL LIST (TYPE: |(GROUND*)→GROUND|) (SYNTYPE: CONSTANT))

37. (DECL LST (TYPE: |GROUND*|))

;labels: SIMPINFO 
38. (AXIOM |LIST(())=NIL|)

;labels: SIMPINFO 
39. (AXIOM |∀LST.LISTP LIST(LST)|)

;labels: SIMPINFO LISTDEF 
40. (AXIOM |∀X LST.LIST(X,LST)=X.LIST(LST)|)

41. (DECL APPEND (TYPE: |(GROUND⊗GROUND⊗(GROUND*))→GROUND|) (SYNTYPE: CONSTANT)
      (ASSOCIATIVITY: BOTH) (INFIXNAME: *) (BINDINGPOWER: 840))

;labels: SIMPINFO APPENDEF 
42. (DEFAX APPEND |∀X U V.NIL*V=V∧X.U*V=X.(U*V)|)

;labels: SIMPINFO LISTAPPEND 
43. (AXIOM |∀U V.LISTP U*V|)

;labels: SIMPINFO 
44. (AXIOM |∀U.U*NIL=U|)

;labels: SIMPINFO 
45. (AXIOM |∀X V.X.NIL*V=X.V|)

46. (DECL (ALLP SOMEP) (SYNTYPE: CONSTANT) (TYPE: |((@PHI)⊗GROUND)→TRUTHVAL|))

;labels: ALLPDEF 
47. (DEFAX ALLP
      |∀PHI X U.ALLP(PHI,NIL)∧
                ALLP(PHI,X.U)=(IF PHI(X) THEN ALLP(PHI,U) ELSE FALSE)|)

;labels: SOMEPDEF 
48. (DEFAX SOMEP
      |∀PHI X U.¬SOMEP(PHI,NIL)∧
                SOMEP(PHI,X.U)=(IF PHI(X) THEN TRUE ELSE SOMEP(PHI,U))|)

;labels: MAPCARDEF 
49. (DEFAX MAPCAR
      |∀FN X U.MAPCAR(FN,NIL)=NIL∧MAPCAR(FN,X.U)=FN(X).MAPCAR(FN,U)|)

50. (DECL (ALIST A0 A1 A2) (TYPE: |GROUND|) (SORT: |ALISTP|))

;labels: SIMPINFO 
51. (AXIOM |∀ALIST.LISTP ALIST|)

52. (AXIOM |∀ALIST.¬NULL ALIST⊃¬ATOM CAR ALIST∧ATOM CAR (CAR ALIST)|)

;labels: MKALIST 
53. (AXIOM |∀XA Y ALIST.ALISTP (XA.Y).ALIST|)

54. (DECL ASSOC (TYPE: |(GROUND⊗GROUND)→GROUND|) (SYNTYPE: CONSTANT))

;labels: ASSOCDEF 
55. (DEFAX ASSOC
      |∀X XA Y ALIST.ASSOC(X,NIL)=NIL∧
                     ASSOC(X,(XA.Y).ALIST)=
                     (IF X=XA THEN XA.Y ELSE ASSOC(X,ALIST))|)

;labels: SIMPINFO 
56. (AXIOM |∀X ALIST.SEXP ASSOC(X,ALIST)|)

57. (DECL MEMBER (TYPE: |(GROUND⊗GROUND)→TRUTHVAL|) (SYNTYPE: CONSTANT))

;labels: MEMBERDEF 
58. (DEFAX MEMBER |∀X Y U.¬MEMBER(X,NIL)∧MEMBER(X,Y.U)=(X=Y∨MEMBER(X,U))|)

59. (DECL SUBST (TYPE: |(GROUND⊗GROUND⊗GROUND)→GROUND|) (SYNTYPE: CONSTANT))

;labels: SUBSTDEF 
60. (DEFAX SUBST
      |∀X Y Z Z1 Z2.(ATOM Z⊃SUBST(X,Y,Z)=(IF Z=Y THEN X ELSE Z))∧
                    SUBST(X,Y,Z1.Z2)=SUBST(X,Y,Z1).SUBST(X,Y,Z2)|)

;labels: SIMPINFO 
61. (UE ((PHI.|λZ.SEXP SUBST(X,Y,Z)|)) SEXPINDUCTION (OPEN SUBST))
∀X3.SEXP SUBST(X,Y,X3)

62. (UE ((PHI.|λZ.SUBST(X,Y,SUBST(X,Y,Z))=SUBST(SUBST(X,Y,X),Y,Z)|))
      SEXPINDUCTION (OPEN SUBST))
∀X4.SUBST(X,Y,SUBST(X,Y,X4))=SUBST(SUBST(X,Y,X),Y,X4)